Runtime Complexity (innermost) proof of /tmp/tmpvasCYP/3.xml

The Runtime Complexity (innermost) of the given CpxTRS could be proven to be BOUNDS(O(1), O(n^1)).

0 CpxTRS

↳1 CpxTrsToCdtProof (BOTH BOUNDS(ID, ID), 0 ms)

↳2 CdtProblem

    ↳3 CdtNarrowingProof (BOTH BOUNDS(ID, ID), 20 ms)

    ↳4 CdtProblem

    ↳5 CdtLeafRemovalProof (BOTH BOUNDS(ID, ID), 0 ms)

    ↳6 CdtProblem

    ↳7 CdtNarrowingProof (BOTH BOUNDS(ID, ID), 0 ms)

    ↳8 CdtProblem

    ↳9 CdtLeafRemovalProof (BOTH BOUNDS(ID, ID), 0 ms)

    ↳10 CdtProblem

    ↳11 CdtNarrowingProof (BOTH BOUNDS(ID, ID), 0 ms)

    ↳12 CdtProblem

    ↳13 CdtLeafRemovalProof (BOTH BOUNDS(ID, ID), 0 ms)

    ↳14 CdtProblem

    ↳15 CdtNarrowingProof (BOTH BOUNDS(ID, ID), 0 ms)

    ↳16 CdtProblem

    ↳17 CdtNarrowingProof (BOTH BOUNDS(ID, ID), 0 ms)

    ↳18 CdtProblem

    ↳19 CdtLeafRemovalProof (BOTH BOUNDS(ID, ID), 0 ms)

    ↳20 CdtProblem

    ↳21 CdtNarrowingProof (BOTH BOUNDS(ID, ID), 0 ms)

    ↳22 CdtProblem

    ↳23 CdtLeafRemovalProof (BOTH BOUNDS(ID, ID), 0 ms)

    ↳24 CdtProblem

    ↳25 CdtNarrowingProof (BOTH BOUNDS(ID, ID), 0 ms)

    ↳26 CdtProblem

↳27 CpxTrsMatchBoundsTAProof (⇔, 0 ms)

↳28 BOUNDS(O(1), O(n^1))

(0) Obligation:

Runtime Complexity TRS:
The TRS R consists of the following rules:

a(0, b(0, x)) → b(0, a(0, x))
a(0, x) → b(0, b(0, x))
a(0, a(1, a(x, y))) → a(1, a(0, a(x, y)))
b(0, a(1, a(x, y))) → b(1, a(0, a(x, y)))
a(0, a(x, y)) → a(1, a(1, a(x, y)))

Rewrite Strategy: INNERMOST

(1) CpxTrsToCdtProof (BOTH BOUNDS(ID, ID) transformation)

Converted CpxTRS to CDT

(2) Obligation:

Complexity Dependency Tuples Problem
Rules:

a(0, b(0, z0)) → b(0, a(0, z0))
a(0, z0) → b(0, b(0, z0))
a(0, a(1, a(z0, z1))) → a(1, a(0, a(z0, z1)))
a(0, a(z0, z1)) → a(1, a(1, a(z0, z1)))
b(0, a(1, a(z0, z1))) → b(1, a(0, a(z0, z1)))

Tuples:

A(0, b(0, z0)) → c(B(0, a(0, z0)), A(0, z0))
A(0, z0) → c1(B(0, b(0, z0)), B(0, z0))
A(0, a(1, a(z0, z1))) → c2(A(1, a(0, a(z0, z1))), A(0, a(z0, z1)), A(z0, z1))
A(0, a(z0, z1)) → c3(A(1, a(1, a(z0, z1))), A(1, a(z0, z1)), A(z0, z1))
B(0, a(1, a(z0, z1))) → c4(B(1, a(0, a(z0, z1))), A(0, a(z0, z1)), A(z0, z1))

S tuples:

A(0, b(0, z0)) → c(B(0, a(0, z0)), A(0, z0))
A(0, z0) → c1(B(0, b(0, z0)), B(0, z0))
A(0, a(1, a(z0, z1))) → c2(A(1, a(0, a(z0, z1))), A(0, a(z0, z1)), A(z0, z1))
A(0, a(z0, z1)) → c3(A(1, a(1, a(z0, z1))), A(1, a(z0, z1)), A(z0, z1))
B(0, a(1, a(z0, z1))) → c4(B(1, a(0, a(z0, z1))), A(0, a(z0, z1)), A(z0, z1))

K tuples:none
Defined Rule Symbols:

a, b

Defined Pair Symbols:

A, B

Compound Symbols:

c, c1, c2, c3, c4

(3) CdtNarrowingProof (BOTH BOUNDS(ID, ID) transformation)

Use narrowing to replace A(0, b(0, z0)) → c(B(0, a(0, z0)), A(0, z0)) by

A(0, b(0, b(0, z0))) → c(B(0, b(0, a(0, z0))), A(0, b(0, z0)))
A(0, b(0, z0)) → c(B(0, b(0, b(0, z0))), A(0, z0))
A(0, b(0, a(z0, z1))) → c(B(0, a(1, a(1, a(z0, z1)))), A(0, a(z0, z1)))
A(0, b(0, x0)) → c

(4) Obligation:

Complexity Dependency Tuples Problem
Rules:

a(0, b(0, z0)) → b(0, a(0, z0))
a(0, z0) → b(0, b(0, z0))
a(0, a(1, a(z0, z1))) → a(1, a(0, a(z0, z1)))
a(0, a(z0, z1)) → a(1, a(1, a(z0, z1)))
b(0, a(1, a(z0, z1))) → b(1, a(0, a(z0, z1)))

Tuples:

A(0, z0) → c1(B(0, b(0, z0)), B(0, z0))
A(0, a(1, a(z0, z1))) → c2(A(1, a(0, a(z0, z1))), A(0, a(z0, z1)), A(z0, z1))
A(0, a(z0, z1)) → c3(A(1, a(1, a(z0, z1))), A(1, a(z0, z1)), A(z0, z1))
B(0, a(1, a(z0, z1))) → c4(B(1, a(0, a(z0, z1))), A(0, a(z0, z1)), A(z0, z1))
A(0, b(0, b(0, z0))) → c(B(0, b(0, a(0, z0))), A(0, b(0, z0)))
A(0, b(0, z0)) → c(B(0, b(0, b(0, z0))), A(0, z0))
A(0, b(0, a(z0, z1))) → c(B(0, a(1, a(1, a(z0, z1)))), A(0, a(z0, z1)))
A(0, b(0, x0)) → c

S tuples:

A(0, z0) → c1(B(0, b(0, z0)), B(0, z0))
A(0, a(1, a(z0, z1))) → c2(A(1, a(0, a(z0, z1))), A(0, a(z0, z1)), A(z0, z1))
A(0, a(z0, z1)) → c3(A(1, a(1, a(z0, z1))), A(1, a(z0, z1)), A(z0, z1))
B(0, a(1, a(z0, z1))) → c4(B(1, a(0, a(z0, z1))), A(0, a(z0, z1)), A(z0, z1))
A(0, b(0, b(0, z0))) → c(B(0, b(0, a(0, z0))), A(0, b(0, z0)))
A(0, b(0, z0)) → c(B(0, b(0, b(0, z0))), A(0, z0))
A(0, b(0, a(z0, z1))) → c(B(0, a(1, a(1, a(z0, z1)))), A(0, a(z0, z1)))
A(0, b(0, x0)) → c

K tuples:none
Defined Rule Symbols:

a, b

Defined Pair Symbols:

A, B

Compound Symbols:

c1, c2, c3, c4, c, c

(5) CdtLeafRemovalProof (BOTH BOUNDS(ID, ID) transformation)

Removed 1 trailing nodes:

A(0, b(0, x0)) → c

(6) Obligation:

Complexity Dependency Tuples Problem
Rules:

a(0, b(0, z0)) → b(0, a(0, z0))
a(0, z0) → b(0, b(0, z0))
a(0, a(1, a(z0, z1))) → a(1, a(0, a(z0, z1)))
a(0, a(z0, z1)) → a(1, a(1, a(z0, z1)))
b(0, a(1, a(z0, z1))) → b(1, a(0, a(z0, z1)))

Tuples:

A(0, z0) → c1(B(0, b(0, z0)), B(0, z0))
A(0, a(1, a(z0, z1))) → c2(A(1, a(0, a(z0, z1))), A(0, a(z0, z1)), A(z0, z1))
A(0, a(z0, z1)) → c3(A(1, a(1, a(z0, z1))), A(1, a(z0, z1)), A(z0, z1))
B(0, a(1, a(z0, z1))) → c4(B(1, a(0, a(z0, z1))), A(0, a(z0, z1)), A(z0, z1))
A(0, b(0, b(0, z0))) → c(B(0, b(0, a(0, z0))), A(0, b(0, z0)))
A(0, b(0, z0)) → c(B(0, b(0, b(0, z0))), A(0, z0))
A(0, b(0, a(z0, z1))) → c(B(0, a(1, a(1, a(z0, z1)))), A(0, a(z0, z1)))

S tuples:

A(0, z0) → c1(B(0, b(0, z0)), B(0, z0))
A(0, a(1, a(z0, z1))) → c2(A(1, a(0, a(z0, z1))), A(0, a(z0, z1)), A(z0, z1))
A(0, a(z0, z1)) → c3(A(1, a(1, a(z0, z1))), A(1, a(z0, z1)), A(z0, z1))
B(0, a(1, a(z0, z1))) → c4(B(1, a(0, a(z0, z1))), A(0, a(z0, z1)), A(z0, z1))
A(0, b(0, b(0, z0))) → c(B(0, b(0, a(0, z0))), A(0, b(0, z0)))
A(0, b(0, z0)) → c(B(0, b(0, b(0, z0))), A(0, z0))
A(0, b(0, a(z0, z1))) → c(B(0, a(1, a(1, a(z0, z1)))), A(0, a(z0, z1)))

K tuples:none
Defined Rule Symbols:

a, b

Defined Pair Symbols:

A, B

Compound Symbols:

c1, c2, c3, c4, c

(7) CdtNarrowingProof (BOTH BOUNDS(ID, ID) transformation)

Use narrowing to replace A(0, z0) → c1(B(0, b(0, z0)), B(0, z0)) by

A(0, a(1, a(z0, z1))) → c1(B(0, b(1, a(0, a(z0, z1)))), B(0, a(1, a(z0, z1))))
A(0, x0) → c1

(8) Obligation:

Complexity Dependency Tuples Problem
Rules:

a(0, b(0, z0)) → b(0, a(0, z0))
a(0, z0) → b(0, b(0, z0))
a(0, a(1, a(z0, z1))) → a(1, a(0, a(z0, z1)))
a(0, a(z0, z1)) → a(1, a(1, a(z0, z1)))
b(0, a(1, a(z0, z1))) → b(1, a(0, a(z0, z1)))

Tuples:

A(0, a(1, a(z0, z1))) → c2(A(1, a(0, a(z0, z1))), A(0, a(z0, z1)), A(z0, z1))
A(0, a(z0, z1)) → c3(A(1, a(1, a(z0, z1))), A(1, a(z0, z1)), A(z0, z1))
B(0, a(1, a(z0, z1))) → c4(B(1, a(0, a(z0, z1))), A(0, a(z0, z1)), A(z0, z1))
A(0, b(0, b(0, z0))) → c(B(0, b(0, a(0, z0))), A(0, b(0, z0)))
A(0, b(0, z0)) → c(B(0, b(0, b(0, z0))), A(0, z0))
A(0, b(0, a(z0, z1))) → c(B(0, a(1, a(1, a(z0, z1)))), A(0, a(z0, z1)))
A(0, a(1, a(z0, z1))) → c1(B(0, b(1, a(0, a(z0, z1)))), B(0, a(1, a(z0, z1))))
A(0, x0) → c1

S tuples:

A(0, a(1, a(z0, z1))) → c2(A(1, a(0, a(z0, z1))), A(0, a(z0, z1)), A(z0, z1))
A(0, a(z0, z1)) → c3(A(1, a(1, a(z0, z1))), A(1, a(z0, z1)), A(z0, z1))
B(0, a(1, a(z0, z1))) → c4(B(1, a(0, a(z0, z1))), A(0, a(z0, z1)), A(z0, z1))
A(0, b(0, b(0, z0))) → c(B(0, b(0, a(0, z0))), A(0, b(0, z0)))
A(0, b(0, z0)) → c(B(0, b(0, b(0, z0))), A(0, z0))
A(0, b(0, a(z0, z1))) → c(B(0, a(1, a(1, a(z0, z1)))), A(0, a(z0, z1)))
A(0, a(1, a(z0, z1))) → c1(B(0, b(1, a(0, a(z0, z1)))), B(0, a(1, a(z0, z1))))
A(0, x0) → c1

K tuples:none
Defined Rule Symbols:

a, b

Defined Pair Symbols:

A, B

Compound Symbols:

c2, c3, c4, c, c1, c1

(9) CdtLeafRemovalProof (BOTH BOUNDS(ID, ID) transformation)

Removed 1 trailing nodes:

A(0, x0) → c1

(10) Obligation:

Complexity Dependency Tuples Problem
Rules:

a(0, b(0, z0)) → b(0, a(0, z0))
a(0, z0) → b(0, b(0, z0))
a(0, a(1, a(z0, z1))) → a(1, a(0, a(z0, z1)))
a(0, a(z0, z1)) → a(1, a(1, a(z0, z1)))
b(0, a(1, a(z0, z1))) → b(1, a(0, a(z0, z1)))

Tuples:

A(0, a(1, a(z0, z1))) → c2(A(1, a(0, a(z0, z1))), A(0, a(z0, z1)), A(z0, z1))
A(0, a(z0, z1)) → c3(A(1, a(1, a(z0, z1))), A(1, a(z0, z1)), A(z0, z1))
B(0, a(1, a(z0, z1))) → c4(B(1, a(0, a(z0, z1))), A(0, a(z0, z1)), A(z0, z1))
A(0, b(0, b(0, z0))) → c(B(0, b(0, a(0, z0))), A(0, b(0, z0)))
A(0, b(0, z0)) → c(B(0, b(0, b(0, z0))), A(0, z0))
A(0, b(0, a(z0, z1))) → c(B(0, a(1, a(1, a(z0, z1)))), A(0, a(z0, z1)))
A(0, a(1, a(z0, z1))) → c1(B(0, b(1, a(0, a(z0, z1)))), B(0, a(1, a(z0, z1))))

S tuples:

A(0, a(1, a(z0, z1))) → c2(A(1, a(0, a(z0, z1))), A(0, a(z0, z1)), A(z0, z1))
A(0, a(z0, z1)) → c3(A(1, a(1, a(z0, z1))), A(1, a(z0, z1)), A(z0, z1))
B(0, a(1, a(z0, z1))) → c4(B(1, a(0, a(z0, z1))), A(0, a(z0, z1)), A(z0, z1))
A(0, b(0, b(0, z0))) → c(B(0, b(0, a(0, z0))), A(0, b(0, z0)))
A(0, b(0, z0)) → c(B(0, b(0, b(0, z0))), A(0, z0))
A(0, b(0, a(z0, z1))) → c(B(0, a(1, a(1, a(z0, z1)))), A(0, a(z0, z1)))
A(0, a(1, a(z0, z1))) → c1(B(0, b(1, a(0, a(z0, z1)))), B(0, a(1, a(z0, z1))))

K tuples:none
Defined Rule Symbols:

a, b

Defined Pair Symbols:

A, B

Compound Symbols:

c2, c3, c4, c, c1

(11) CdtNarrowingProof (BOTH BOUNDS(ID, ID) transformation)

Use narrowing to replace A(0, a(1, a(z0, z1))) → c2(A(1, a(0, a(z0, z1))), A(0, a(z0, z1)), A(z0, z1)) by

A(0, a(1, a(x0, x1))) → c2(A(1, b(0, b(0, a(x0, x1)))), A(0, a(x0, x1)), A(x0, x1))
A(0, a(1, a(1, a(z0, z1)))) → c2(A(1, a(1, a(0, a(z0, z1)))), A(0, a(1, a(z0, z1))), A(1, a(z0, z1)))
A(0, a(1, a(z0, z1))) → c2(A(1, a(1, a(1, a(z0, z1)))), A(0, a(z0, z1)), A(z0, z1))
A(0, a(1, a(x0, x1))) → c2

(12) Obligation:

Complexity Dependency Tuples Problem
Rules:

a(0, b(0, z0)) → b(0, a(0, z0))
a(0, z0) → b(0, b(0, z0))
a(0, a(1, a(z0, z1))) → a(1, a(0, a(z0, z1)))
a(0, a(z0, z1)) → a(1, a(1, a(z0, z1)))
b(0, a(1, a(z0, z1))) → b(1, a(0, a(z0, z1)))

Tuples:

A(0, a(z0, z1)) → c3(A(1, a(1, a(z0, z1))), A(1, a(z0, z1)), A(z0, z1))
B(0, a(1, a(z0, z1))) → c4(B(1, a(0, a(z0, z1))), A(0, a(z0, z1)), A(z0, z1))
A(0, b(0, b(0, z0))) → c(B(0, b(0, a(0, z0))), A(0, b(0, z0)))
A(0, b(0, z0)) → c(B(0, b(0, b(0, z0))), A(0, z0))
A(0, b(0, a(z0, z1))) → c(B(0, a(1, a(1, a(z0, z1)))), A(0, a(z0, z1)))
A(0, a(1, a(z0, z1))) → c1(B(0, b(1, a(0, a(z0, z1)))), B(0, a(1, a(z0, z1))))
A(0, a(1, a(x0, x1))) → c2(A(1, b(0, b(0, a(x0, x1)))), A(0, a(x0, x1)), A(x0, x1))
A(0, a(1, a(1, a(z0, z1)))) → c2(A(1, a(1, a(0, a(z0, z1)))), A(0, a(1, a(z0, z1))), A(1, a(z0, z1)))
A(0, a(1, a(z0, z1))) → c2(A(1, a(1, a(1, a(z0, z1)))), A(0, a(z0, z1)), A(z0, z1))
A(0, a(1, a(x0, x1))) → c2

S tuples:

A(0, a(z0, z1)) → c3(A(1, a(1, a(z0, z1))), A(1, a(z0, z1)), A(z0, z1))
B(0, a(1, a(z0, z1))) → c4(B(1, a(0, a(z0, z1))), A(0, a(z0, z1)), A(z0, z1))
A(0, b(0, b(0, z0))) → c(B(0, b(0, a(0, z0))), A(0, b(0, z0)))
A(0, b(0, z0)) → c(B(0, b(0, b(0, z0))), A(0, z0))
A(0, b(0, a(z0, z1))) → c(B(0, a(1, a(1, a(z0, z1)))), A(0, a(z0, z1)))
A(0, a(1, a(z0, z1))) → c1(B(0, b(1, a(0, a(z0, z1)))), B(0, a(1, a(z0, z1))))
A(0, a(1, a(x0, x1))) → c2(A(1, b(0, b(0, a(x0, x1)))), A(0, a(x0, x1)), A(x0, x1))
A(0, a(1, a(1, a(z0, z1)))) → c2(A(1, a(1, a(0, a(z0, z1)))), A(0, a(1, a(z0, z1))), A(1, a(z0, z1)))
A(0, a(1, a(z0, z1))) → c2(A(1, a(1, a(1, a(z0, z1)))), A(0, a(z0, z1)), A(z0, z1))
A(0, a(1, a(x0, x1))) → c2

K tuples:none
Defined Rule Symbols:

a, b

Defined Pair Symbols:

A, B

Compound Symbols:

c3, c4, c, c1, c2, c2

(13) CdtLeafRemovalProof (BOTH BOUNDS(ID, ID) transformation)

Removed 1 trailing nodes:

A(0, a(1, a(x0, x1))) → c2

(14) Obligation:

Complexity Dependency Tuples Problem
Rules:

a(0, b(0, z0)) → b(0, a(0, z0))
a(0, z0) → b(0, b(0, z0))
a(0, a(1, a(z0, z1))) → a(1, a(0, a(z0, z1)))
a(0, a(z0, z1)) → a(1, a(1, a(z0, z1)))
b(0, a(1, a(z0, z1))) → b(1, a(0, a(z0, z1)))

Tuples:

A(0, a(z0, z1)) → c3(A(1, a(1, a(z0, z1))), A(1, a(z0, z1)), A(z0, z1))
B(0, a(1, a(z0, z1))) → c4(B(1, a(0, a(z0, z1))), A(0, a(z0, z1)), A(z0, z1))
A(0, b(0, b(0, z0))) → c(B(0, b(0, a(0, z0))), A(0, b(0, z0)))
A(0, b(0, z0)) → c(B(0, b(0, b(0, z0))), A(0, z0))
A(0, b(0, a(z0, z1))) → c(B(0, a(1, a(1, a(z0, z1)))), A(0, a(z0, z1)))
A(0, a(1, a(z0, z1))) → c1(B(0, b(1, a(0, a(z0, z1)))), B(0, a(1, a(z0, z1))))
A(0, a(1, a(x0, x1))) → c2(A(1, b(0, b(0, a(x0, x1)))), A(0, a(x0, x1)), A(x0, x1))
A(0, a(1, a(1, a(z0, z1)))) → c2(A(1, a(1, a(0, a(z0, z1)))), A(0, a(1, a(z0, z1))), A(1, a(z0, z1)))
A(0, a(1, a(z0, z1))) → c2(A(1, a(1, a(1, a(z0, z1)))), A(0, a(z0, z1)), A(z0, z1))

S tuples:

A(0, a(z0, z1)) → c3(A(1, a(1, a(z0, z1))), A(1, a(z0, z1)), A(z0, z1))
B(0, a(1, a(z0, z1))) → c4(B(1, a(0, a(z0, z1))), A(0, a(z0, z1)), A(z0, z1))
A(0, b(0, b(0, z0))) → c(B(0, b(0, a(0, z0))), A(0, b(0, z0)))
A(0, b(0, z0)) → c(B(0, b(0, b(0, z0))), A(0, z0))
A(0, b(0, a(z0, z1))) → c(B(0, a(1, a(1, a(z0, z1)))), A(0, a(z0, z1)))
A(0, a(1, a(z0, z1))) → c1(B(0, b(1, a(0, a(z0, z1)))), B(0, a(1, a(z0, z1))))
A(0, a(1, a(x0, x1))) → c2(A(1, b(0, b(0, a(x0, x1)))), A(0, a(x0, x1)), A(x0, x1))
A(0, a(1, a(1, a(z0, z1)))) → c2(A(1, a(1, a(0, a(z0, z1)))), A(0, a(1, a(z0, z1))), A(1, a(z0, z1)))
A(0, a(1, a(z0, z1))) → c2(A(1, a(1, a(1, a(z0, z1)))), A(0, a(z0, z1)), A(z0, z1))

K tuples:none
Defined Rule Symbols:

a, b

Defined Pair Symbols:

A, B

Compound Symbols:

c3, c4, c, c1, c2

(15) CdtNarrowingProof (BOTH BOUNDS(ID, ID) transformation)

Use narrowing to replace A(0, a(z0, z1)) → c3(A(1, a(1, a(z0, z1))), A(1, a(z0, z1)), A(z0, z1)) by

A(0, a(x0, x1)) → c3(A(x0, x1))

(16) Obligation:

Complexity Dependency Tuples Problem
Rules:

a(0, b(0, z0)) → b(0, a(0, z0))
a(0, z0) → b(0, b(0, z0))
a(0, a(1, a(z0, z1))) → a(1, a(0, a(z0, z1)))
a(0, a(z0, z1)) → a(1, a(1, a(z0, z1)))
b(0, a(1, a(z0, z1))) → b(1, a(0, a(z0, z1)))

Tuples:

B(0, a(1, a(z0, z1))) → c4(B(1, a(0, a(z0, z1))), A(0, a(z0, z1)), A(z0, z1))
A(0, b(0, b(0, z0))) → c(B(0, b(0, a(0, z0))), A(0, b(0, z0)))
A(0, b(0, z0)) → c(B(0, b(0, b(0, z0))), A(0, z0))
A(0, b(0, a(z0, z1))) → c(B(0, a(1, a(1, a(z0, z1)))), A(0, a(z0, z1)))
A(0, a(1, a(z0, z1))) → c1(B(0, b(1, a(0, a(z0, z1)))), B(0, a(1, a(z0, z1))))
A(0, a(1, a(x0, x1))) → c2(A(1, b(0, b(0, a(x0, x1)))), A(0, a(x0, x1)), A(x0, x1))
A(0, a(1, a(1, a(z0, z1)))) → c2(A(1, a(1, a(0, a(z0, z1)))), A(0, a(1, a(z0, z1))), A(1, a(z0, z1)))
A(0, a(1, a(z0, z1))) → c2(A(1, a(1, a(1, a(z0, z1)))), A(0, a(z0, z1)), A(z0, z1))
A(0, a(x0, x1)) → c3(A(x0, x1))

S tuples:

B(0, a(1, a(z0, z1))) → c4(B(1, a(0, a(z0, z1))), A(0, a(z0, z1)), A(z0, z1))
A(0, b(0, b(0, z0))) → c(B(0, b(0, a(0, z0))), A(0, b(0, z0)))
A(0, b(0, z0)) → c(B(0, b(0, b(0, z0))), A(0, z0))
A(0, b(0, a(z0, z1))) → c(B(0, a(1, a(1, a(z0, z1)))), A(0, a(z0, z1)))
A(0, a(1, a(z0, z1))) → c1(B(0, b(1, a(0, a(z0, z1)))), B(0, a(1, a(z0, z1))))
A(0, a(1, a(x0, x1))) → c2(A(1, b(0, b(0, a(x0, x1)))), A(0, a(x0, x1)), A(x0, x1))
A(0, a(1, a(1, a(z0, z1)))) → c2(A(1, a(1, a(0, a(z0, z1)))), A(0, a(1, a(z0, z1))), A(1, a(z0, z1)))
A(0, a(1, a(z0, z1))) → c2(A(1, a(1, a(1, a(z0, z1)))), A(0, a(z0, z1)), A(z0, z1))
A(0, a(x0, x1)) → c3(A(x0, x1))

K tuples:none
Defined Rule Symbols:

a, b

Defined Pair Symbols:

B, A

Compound Symbols:

c4, c, c1, c2, c3

(17) CdtNarrowingProof (BOTH BOUNDS(ID, ID) transformation)

Use narrowing to replace B(0, a(1, a(z0, z1))) → c4(B(1, a(0, a(z0, z1))), A(0, a(z0, z1)), A(z0, z1)) by

B(0, a(1, a(x0, x1))) → c4(B(1, b(0, b(0, a(x0, x1)))), A(0, a(x0, x1)), A(x0, x1))
B(0, a(1, a(1, a(z0, z1)))) → c4(B(1, a(1, a(0, a(z0, z1)))), A(0, a(1, a(z0, z1))), A(1, a(z0, z1)))
B(0, a(1, a(z0, z1))) → c4(B(1, a(1, a(1, a(z0, z1)))), A(0, a(z0, z1)), A(z0, z1))
B(0, a(1, a(x0, x1))) → c4

(18) Obligation:

Complexity Dependency Tuples Problem
Rules:

a(0, b(0, z0)) → b(0, a(0, z0))
a(0, z0) → b(0, b(0, z0))
a(0, a(1, a(z0, z1))) → a(1, a(0, a(z0, z1)))
a(0, a(z0, z1)) → a(1, a(1, a(z0, z1)))
b(0, a(1, a(z0, z1))) → b(1, a(0, a(z0, z1)))

Tuples:

A(0, b(0, b(0, z0))) → c(B(0, b(0, a(0, z0))), A(0, b(0, z0)))
A(0, b(0, z0)) → c(B(0, b(0, b(0, z0))), A(0, z0))
A(0, b(0, a(z0, z1))) → c(B(0, a(1, a(1, a(z0, z1)))), A(0, a(z0, z1)))
A(0, a(1, a(z0, z1))) → c1(B(0, b(1, a(0, a(z0, z1)))), B(0, a(1, a(z0, z1))))
A(0, a(1, a(x0, x1))) → c2(A(1, b(0, b(0, a(x0, x1)))), A(0, a(x0, x1)), A(x0, x1))
A(0, a(1, a(1, a(z0, z1)))) → c2(A(1, a(1, a(0, a(z0, z1)))), A(0, a(1, a(z0, z1))), A(1, a(z0, z1)))
A(0, a(1, a(z0, z1))) → c2(A(1, a(1, a(1, a(z0, z1)))), A(0, a(z0, z1)), A(z0, z1))
A(0, a(x0, x1)) → c3(A(x0, x1))
B(0, a(1, a(x0, x1))) → c4(B(1, b(0, b(0, a(x0, x1)))), A(0, a(x0, x1)), A(x0, x1))
B(0, a(1, a(1, a(z0, z1)))) → c4(B(1, a(1, a(0, a(z0, z1)))), A(0, a(1, a(z0, z1))), A(1, a(z0, z1)))
B(0, a(1, a(z0, z1))) → c4(B(1, a(1, a(1, a(z0, z1)))), A(0, a(z0, z1)), A(z0, z1))
B(0, a(1, a(x0, x1))) → c4

S tuples:

A(0, b(0, b(0, z0))) → c(B(0, b(0, a(0, z0))), A(0, b(0, z0)))
A(0, b(0, z0)) → c(B(0, b(0, b(0, z0))), A(0, z0))
A(0, b(0, a(z0, z1))) → c(B(0, a(1, a(1, a(z0, z1)))), A(0, a(z0, z1)))
A(0, a(1, a(z0, z1))) → c1(B(0, b(1, a(0, a(z0, z1)))), B(0, a(1, a(z0, z1))))
A(0, a(1, a(x0, x1))) → c2(A(1, b(0, b(0, a(x0, x1)))), A(0, a(x0, x1)), A(x0, x1))
A(0, a(1, a(1, a(z0, z1)))) → c2(A(1, a(1, a(0, a(z0, z1)))), A(0, a(1, a(z0, z1))), A(1, a(z0, z1)))
A(0, a(1, a(z0, z1))) → c2(A(1, a(1, a(1, a(z0, z1)))), A(0, a(z0, z1)), A(z0, z1))
A(0, a(x0, x1)) → c3(A(x0, x1))
B(0, a(1, a(x0, x1))) → c4(B(1, b(0, b(0, a(x0, x1)))), A(0, a(x0, x1)), A(x0, x1))
B(0, a(1, a(1, a(z0, z1)))) → c4(B(1, a(1, a(0, a(z0, z1)))), A(0, a(1, a(z0, z1))), A(1, a(z0, z1)))
B(0, a(1, a(z0, z1))) → c4(B(1, a(1, a(1, a(z0, z1)))), A(0, a(z0, z1)), A(z0, z1))
B(0, a(1, a(x0, x1))) → c4

K tuples:none
Defined Rule Symbols:

a, b

Defined Pair Symbols:

A, B

Compound Symbols:

c, c1, c2, c3, c4, c4

(19) CdtLeafRemovalProof (BOTH BOUNDS(ID, ID) transformation)

Removed 1 trailing nodes:

B(0, a(1, a(x0, x1))) → c4

(20) Obligation:

Complexity Dependency Tuples Problem
Rules:

a(0, b(0, z0)) → b(0, a(0, z0))
a(0, z0) → b(0, b(0, z0))
a(0, a(1, a(z0, z1))) → a(1, a(0, a(z0, z1)))
a(0, a(z0, z1)) → a(1, a(1, a(z0, z1)))
b(0, a(1, a(z0, z1))) → b(1, a(0, a(z0, z1)))

Tuples:

A(0, b(0, b(0, z0))) → c(B(0, b(0, a(0, z0))), A(0, b(0, z0)))
A(0, b(0, z0)) → c(B(0, b(0, b(0, z0))), A(0, z0))
A(0, b(0, a(z0, z1))) → c(B(0, a(1, a(1, a(z0, z1)))), A(0, a(z0, z1)))
A(0, a(1, a(z0, z1))) → c1(B(0, b(1, a(0, a(z0, z1)))), B(0, a(1, a(z0, z1))))
A(0, a(1, a(x0, x1))) → c2(A(1, b(0, b(0, a(x0, x1)))), A(0, a(x0, x1)), A(x0, x1))
A(0, a(1, a(1, a(z0, z1)))) → c2(A(1, a(1, a(0, a(z0, z1)))), A(0, a(1, a(z0, z1))), A(1, a(z0, z1)))
A(0, a(1, a(z0, z1))) → c2(A(1, a(1, a(1, a(z0, z1)))), A(0, a(z0, z1)), A(z0, z1))
A(0, a(x0, x1)) → c3(A(x0, x1))
B(0, a(1, a(x0, x1))) → c4(B(1, b(0, b(0, a(x0, x1)))), A(0, a(x0, x1)), A(x0, x1))
B(0, a(1, a(1, a(z0, z1)))) → c4(B(1, a(1, a(0, a(z0, z1)))), A(0, a(1, a(z0, z1))), A(1, a(z0, z1)))
B(0, a(1, a(z0, z1))) → c4(B(1, a(1, a(1, a(z0, z1)))), A(0, a(z0, z1)), A(z0, z1))

S tuples:

A(0, b(0, b(0, z0))) → c(B(0, b(0, a(0, z0))), A(0, b(0, z0)))
A(0, b(0, z0)) → c(B(0, b(0, b(0, z0))), A(0, z0))
A(0, b(0, a(z0, z1))) → c(B(0, a(1, a(1, a(z0, z1)))), A(0, a(z0, z1)))
A(0, a(1, a(z0, z1))) → c1(B(0, b(1, a(0, a(z0, z1)))), B(0, a(1, a(z0, z1))))
A(0, a(1, a(x0, x1))) → c2(A(1, b(0, b(0, a(x0, x1)))), A(0, a(x0, x1)), A(x0, x1))
A(0, a(1, a(1, a(z0, z1)))) → c2(A(1, a(1, a(0, a(z0, z1)))), A(0, a(1, a(z0, z1))), A(1, a(z0, z1)))
A(0, a(1, a(z0, z1))) → c2(A(1, a(1, a(1, a(z0, z1)))), A(0, a(z0, z1)), A(z0, z1))
A(0, a(x0, x1)) → c3(A(x0, x1))
B(0, a(1, a(x0, x1))) → c4(B(1, b(0, b(0, a(x0, x1)))), A(0, a(x0, x1)), A(x0, x1))
B(0, a(1, a(1, a(z0, z1)))) → c4(B(1, a(1, a(0, a(z0, z1)))), A(0, a(1, a(z0, z1))), A(1, a(z0, z1)))
B(0, a(1, a(z0, z1))) → c4(B(1, a(1, a(1, a(z0, z1)))), A(0, a(z0, z1)), A(z0, z1))

K tuples:none
Defined Rule Symbols:

a, b

Defined Pair Symbols:

A, B

Compound Symbols:

c, c1, c2, c3, c4

(21) CdtNarrowingProof (BOTH BOUNDS(ID, ID) transformation)

Use narrowing to replace A(0, b(0, b(0, z0))) → c(B(0, b(0, a(0, z0))), A(0, b(0, z0))) by

A(0, b(0, b(0, b(0, z0)))) → c(B(0, b(0, b(0, a(0, z0)))), A(0, b(0, b(0, z0))))
A(0, b(0, b(0, z0))) → c(B(0, b(0, b(0, b(0, z0)))), A(0, b(0, z0)))
A(0, b(0, b(0, a(z0, z1)))) → c(B(0, b(0, a(1, a(1, a(z0, z1))))), A(0, b(0, a(z0, z1))))
A(0, b(0, b(0, x0))) → c

(22) Obligation:

Complexity Dependency Tuples Problem
Rules:

a(0, b(0, z0)) → b(0, a(0, z0))
a(0, z0) → b(0, b(0, z0))
a(0, a(1, a(z0, z1))) → a(1, a(0, a(z0, z1)))
a(0, a(z0, z1)) → a(1, a(1, a(z0, z1)))
b(0, a(1, a(z0, z1))) → b(1, a(0, a(z0, z1)))

Tuples:

A(0, b(0, z0)) → c(B(0, b(0, b(0, z0))), A(0, z0))
A(0, b(0, a(z0, z1))) → c(B(0, a(1, a(1, a(z0, z1)))), A(0, a(z0, z1)))
A(0, a(1, a(z0, z1))) → c1(B(0, b(1, a(0, a(z0, z1)))), B(0, a(1, a(z0, z1))))
A(0, a(1, a(x0, x1))) → c2(A(1, b(0, b(0, a(x0, x1)))), A(0, a(x0, x1)), A(x0, x1))
A(0, a(1, a(1, a(z0, z1)))) → c2(A(1, a(1, a(0, a(z0, z1)))), A(0, a(1, a(z0, z1))), A(1, a(z0, z1)))
A(0, a(1, a(z0, z1))) → c2(A(1, a(1, a(1, a(z0, z1)))), A(0, a(z0, z1)), A(z0, z1))
A(0, a(x0, x1)) → c3(A(x0, x1))
B(0, a(1, a(x0, x1))) → c4(B(1, b(0, b(0, a(x0, x1)))), A(0, a(x0, x1)), A(x0, x1))
B(0, a(1, a(1, a(z0, z1)))) → c4(B(1, a(1, a(0, a(z0, z1)))), A(0, a(1, a(z0, z1))), A(1, a(z0, z1)))
B(0, a(1, a(z0, z1))) → c4(B(1, a(1, a(1, a(z0, z1)))), A(0, a(z0, z1)), A(z0, z1))
A(0, b(0, b(0, b(0, z0)))) → c(B(0, b(0, b(0, a(0, z0)))), A(0, b(0, b(0, z0))))
A(0, b(0, b(0, z0))) → c(B(0, b(0, b(0, b(0, z0)))), A(0, b(0, z0)))
A(0, b(0, b(0, a(z0, z1)))) → c(B(0, b(0, a(1, a(1, a(z0, z1))))), A(0, b(0, a(z0, z1))))
A(0, b(0, b(0, x0))) → c

S tuples:

A(0, b(0, z0)) → c(B(0, b(0, b(0, z0))), A(0, z0))
A(0, b(0, a(z0, z1))) → c(B(0, a(1, a(1, a(z0, z1)))), A(0, a(z0, z1)))
A(0, a(1, a(z0, z1))) → c1(B(0, b(1, a(0, a(z0, z1)))), B(0, a(1, a(z0, z1))))
A(0, a(1, a(x0, x1))) → c2(A(1, b(0, b(0, a(x0, x1)))), A(0, a(x0, x1)), A(x0, x1))
A(0, a(1, a(1, a(z0, z1)))) → c2(A(1, a(1, a(0, a(z0, z1)))), A(0, a(1, a(z0, z1))), A(1, a(z0, z1)))
A(0, a(1, a(z0, z1))) → c2(A(1, a(1, a(1, a(z0, z1)))), A(0, a(z0, z1)), A(z0, z1))
A(0, a(x0, x1)) → c3(A(x0, x1))
B(0, a(1, a(x0, x1))) → c4(B(1, b(0, b(0, a(x0, x1)))), A(0, a(x0, x1)), A(x0, x1))
B(0, a(1, a(1, a(z0, z1)))) → c4(B(1, a(1, a(0, a(z0, z1)))), A(0, a(1, a(z0, z1))), A(1, a(z0, z1)))
B(0, a(1, a(z0, z1))) → c4(B(1, a(1, a(1, a(z0, z1)))), A(0, a(z0, z1)), A(z0, z1))
A(0, b(0, b(0, b(0, z0)))) → c(B(0, b(0, b(0, a(0, z0)))), A(0, b(0, b(0, z0))))
A(0, b(0, b(0, z0))) → c(B(0, b(0, b(0, b(0, z0)))), A(0, b(0, z0)))
A(0, b(0, b(0, a(z0, z1)))) → c(B(0, b(0, a(1, a(1, a(z0, z1))))), A(0, b(0, a(z0, z1))))
A(0, b(0, b(0, x0))) → c

K tuples:none
Defined Rule Symbols:

a, b

Defined Pair Symbols:

A, B

Compound Symbols:

c, c1, c2, c3, c4, c

(23) CdtLeafRemovalProof (BOTH BOUNDS(ID, ID) transformation)

Removed 1 trailing nodes:

A(0, b(0, b(0, x0))) → c

(24) Obligation:

Complexity Dependency Tuples Problem
Rules:

a(0, b(0, z0)) → b(0, a(0, z0))
a(0, z0) → b(0, b(0, z0))
a(0, a(1, a(z0, z1))) → a(1, a(0, a(z0, z1)))
a(0, a(z0, z1)) → a(1, a(1, a(z0, z1)))
b(0, a(1, a(z0, z1))) → b(1, a(0, a(z0, z1)))

Tuples:

A(0, b(0, z0)) → c(B(0, b(0, b(0, z0))), A(0, z0))
A(0, b(0, a(z0, z1))) → c(B(0, a(1, a(1, a(z0, z1)))), A(0, a(z0, z1)))
A(0, a(1, a(z0, z1))) → c1(B(0, b(1, a(0, a(z0, z1)))), B(0, a(1, a(z0, z1))))
A(0, a(1, a(x0, x1))) → c2(A(1, b(0, b(0, a(x0, x1)))), A(0, a(x0, x1)), A(x0, x1))
A(0, a(1, a(1, a(z0, z1)))) → c2(A(1, a(1, a(0, a(z0, z1)))), A(0, a(1, a(z0, z1))), A(1, a(z0, z1)))
A(0, a(1, a(z0, z1))) → c2(A(1, a(1, a(1, a(z0, z1)))), A(0, a(z0, z1)), A(z0, z1))
A(0, a(x0, x1)) → c3(A(x0, x1))
B(0, a(1, a(x0, x1))) → c4(B(1, b(0, b(0, a(x0, x1)))), A(0, a(x0, x1)), A(x0, x1))
B(0, a(1, a(1, a(z0, z1)))) → c4(B(1, a(1, a(0, a(z0, z1)))), A(0, a(1, a(z0, z1))), A(1, a(z0, z1)))
B(0, a(1, a(z0, z1))) → c4(B(1, a(1, a(1, a(z0, z1)))), A(0, a(z0, z1)), A(z0, z1))
A(0, b(0, b(0, b(0, z0)))) → c(B(0, b(0, b(0, a(0, z0)))), A(0, b(0, b(0, z0))))
A(0, b(0, b(0, z0))) → c(B(0, b(0, b(0, b(0, z0)))), A(0, b(0, z0)))
A(0, b(0, b(0, a(z0, z1)))) → c(B(0, b(0, a(1, a(1, a(z0, z1))))), A(0, b(0, a(z0, z1))))

S tuples:

A(0, b(0, z0)) → c(B(0, b(0, b(0, z0))), A(0, z0))
A(0, b(0, a(z0, z1))) → c(B(0, a(1, a(1, a(z0, z1)))), A(0, a(z0, z1)))
A(0, a(1, a(z0, z1))) → c1(B(0, b(1, a(0, a(z0, z1)))), B(0, a(1, a(z0, z1))))
A(0, a(1, a(x0, x1))) → c2(A(1, b(0, b(0, a(x0, x1)))), A(0, a(x0, x1)), A(x0, x1))
A(0, a(1, a(1, a(z0, z1)))) → c2(A(1, a(1, a(0, a(z0, z1)))), A(0, a(1, a(z0, z1))), A(1, a(z0, z1)))
A(0, a(1, a(z0, z1))) → c2(A(1, a(1, a(1, a(z0, z1)))), A(0, a(z0, z1)), A(z0, z1))
A(0, a(x0, x1)) → c3(A(x0, x1))
B(0, a(1, a(x0, x1))) → c4(B(1, b(0, b(0, a(x0, x1)))), A(0, a(x0, x1)), A(x0, x1))
B(0, a(1, a(1, a(z0, z1)))) → c4(B(1, a(1, a(0, a(z0, z1)))), A(0, a(1, a(z0, z1))), A(1, a(z0, z1)))
B(0, a(1, a(z0, z1))) → c4(B(1, a(1, a(1, a(z0, z1)))), A(0, a(z0, z1)), A(z0, z1))
A(0, b(0, b(0, b(0, z0)))) → c(B(0, b(0, b(0, a(0, z0)))), A(0, b(0, b(0, z0))))
A(0, b(0, b(0, z0))) → c(B(0, b(0, b(0, b(0, z0)))), A(0, b(0, z0)))
A(0, b(0, b(0, a(z0, z1)))) → c(B(0, b(0, a(1, a(1, a(z0, z1))))), A(0, b(0, a(z0, z1))))

K tuples:none
Defined Rule Symbols:

a, b

Defined Pair Symbols:

A, B

Compound Symbols:

c, c1, c2, c3, c4

(25) CdtNarrowingProof (BOTH BOUNDS(ID, ID) transformation)

Use narrowing to replace A(0, b(0, z0)) → c(B(0, b(0, b(0, z0))), A(0, z0)) by

A(0, b(0, x0)) → c(A(0, x0))

(26) Obligation:

Complexity Dependency Tuples Problem
Rules:

a(0, b(0, z0)) → b(0, a(0, z0))
a(0, z0) → b(0, b(0, z0))
a(0, a(1, a(z0, z1))) → a(1, a(0, a(z0, z1)))
a(0, a(z0, z1)) → a(1, a(1, a(z0, z1)))
b(0, a(1, a(z0, z1))) → b(1, a(0, a(z0, z1)))

Tuples:

A(0, b(0, a(z0, z1))) → c(B(0, a(1, a(1, a(z0, z1)))), A(0, a(z0, z1)))
A(0, a(1, a(z0, z1))) → c1(B(0, b(1, a(0, a(z0, z1)))), B(0, a(1, a(z0, z1))))
A(0, a(1, a(x0, x1))) → c2(A(1, b(0, b(0, a(x0, x1)))), A(0, a(x0, x1)), A(x0, x1))
A(0, a(1, a(1, a(z0, z1)))) → c2(A(1, a(1, a(0, a(z0, z1)))), A(0, a(1, a(z0, z1))), A(1, a(z0, z1)))
A(0, a(1, a(z0, z1))) → c2(A(1, a(1, a(1, a(z0, z1)))), A(0, a(z0, z1)), A(z0, z1))
A(0, a(x0, x1)) → c3(A(x0, x1))
B(0, a(1, a(x0, x1))) → c4(B(1, b(0, b(0, a(x0, x1)))), A(0, a(x0, x1)), A(x0, x1))
B(0, a(1, a(1, a(z0, z1)))) → c4(B(1, a(1, a(0, a(z0, z1)))), A(0, a(1, a(z0, z1))), A(1, a(z0, z1)))
B(0, a(1, a(z0, z1))) → c4(B(1, a(1, a(1, a(z0, z1)))), A(0, a(z0, z1)), A(z0, z1))
A(0, b(0, b(0, b(0, z0)))) → c(B(0, b(0, b(0, a(0, z0)))), A(0, b(0, b(0, z0))))
A(0, b(0, b(0, z0))) → c(B(0, b(0, b(0, b(0, z0)))), A(0, b(0, z0)))
A(0, b(0, b(0, a(z0, z1)))) → c(B(0, b(0, a(1, a(1, a(z0, z1))))), A(0, b(0, a(z0, z1))))
A(0, b(0, x0)) → c(A(0, x0))

S tuples:

A(0, b(0, a(z0, z1))) → c(B(0, a(1, a(1, a(z0, z1)))), A(0, a(z0, z1)))
A(0, a(1, a(z0, z1))) → c1(B(0, b(1, a(0, a(z0, z1)))), B(0, a(1, a(z0, z1))))
A(0, a(1, a(x0, x1))) → c2(A(1, b(0, b(0, a(x0, x1)))), A(0, a(x0, x1)), A(x0, x1))
A(0, a(1, a(1, a(z0, z1)))) → c2(A(1, a(1, a(0, a(z0, z1)))), A(0, a(1, a(z0, z1))), A(1, a(z0, z1)))
A(0, a(1, a(z0, z1))) → c2(A(1, a(1, a(1, a(z0, z1)))), A(0, a(z0, z1)), A(z0, z1))
A(0, a(x0, x1)) → c3(A(x0, x1))
B(0, a(1, a(x0, x1))) → c4(B(1, b(0, b(0, a(x0, x1)))), A(0, a(x0, x1)), A(x0, x1))
B(0, a(1, a(1, a(z0, z1)))) → c4(B(1, a(1, a(0, a(z0, z1)))), A(0, a(1, a(z0, z1))), A(1, a(z0, z1)))
B(0, a(1, a(z0, z1))) → c4(B(1, a(1, a(1, a(z0, z1)))), A(0, a(z0, z1)), A(z0, z1))
A(0, b(0, b(0, b(0, z0)))) → c(B(0, b(0, b(0, a(0, z0)))), A(0, b(0, b(0, z0))))
A(0, b(0, b(0, z0))) → c(B(0, b(0, b(0, b(0, z0)))), A(0, b(0, z0)))
A(0, b(0, b(0, a(z0, z1)))) → c(B(0, b(0, a(1, a(1, a(z0, z1))))), A(0, b(0, a(z0, z1))))
A(0, b(0, x0)) → c(A(0, x0))

K tuples:none
Defined Rule Symbols:

a, b

Defined Pair Symbols:

A, B

Compound Symbols:

c, c1, c2, c3, c4, c

(27) CpxTrsMatchBoundsTAProof (EQUIVALENT transformation)

A linear upper bound on the runtime complexity of the TRS R could be shown with a Match-Bound[TAB_LEFTLINEAR,TAB_NONLEFTLINEAR] (for contructor-based start-terms) of 1.

The compatible tree automaton used to show the Match-Boundedness (for constructor-based start-terms) is represented by:
final states : [1, 2]
transitions:
00() → 0
10() → 0
a0(0, 0) → 1
b0(0, 0) → 2
01() → 3
b1(3, 0) → 4
b1(3, 4) → 1

(0) Obligation:

(1) CpxTrsToCdtProof (BOTH BOUNDS(ID, ID) transformation)

(2) Obligation:

(3) CdtNarrowingProof (BOTH BOUNDS(ID, ID) transformation)

(4) Obligation:

(5) CdtLeafRemovalProof (BOTH BOUNDS(ID, ID) transformation)

(6) Obligation:

(7) CdtNarrowingProof (BOTH BOUNDS(ID, ID) transformation)

(8) Obligation:

(9) CdtLeafRemovalProof (BOTH BOUNDS(ID, ID) transformation)

(10) Obligation:

(11) CdtNarrowingProof (BOTH BOUNDS(ID, ID) transformation)

(12) Obligation:

(13) CdtLeafRemovalProof (BOTH BOUNDS(ID, ID) transformation)

(14) Obligation:

(15) CdtNarrowingProof (BOTH BOUNDS(ID, ID) transformation)

(16) Obligation:

(17) CdtNarrowingProof (BOTH BOUNDS(ID, ID) transformation)

(18) Obligation:

(19) CdtLeafRemovalProof (BOTH BOUNDS(ID, ID) transformation)

(20) Obligation:

(21) CdtNarrowingProof (BOTH BOUNDS(ID, ID) transformation)

(22) Obligation:

(23) CdtLeafRemovalProof (BOTH BOUNDS(ID, ID) transformation)

(24) Obligation:

(25) CdtNarrowingProof (BOTH BOUNDS(ID, ID) transformation)

(26) Obligation:

(27) CpxTrsMatchBoundsTAProof (EQUIVALENT transformation)

(28) BOUNDS(O(1), O(n^1))